(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(assert (and v3 v1))
(declare-const v17 Bool)
(assert (xor v11 v2 v14 v8 (and v1 v15 v17 v10 v10 v3 v10 v4 v0)))
(push)
(declare-const v18 Bool)
(assert (xor v18 v14 (xor v11 v2 v14 v8 (and v1 v15 v17 v10 v10 v3 v10 v4 v0)) v2 v11))
(check-sat)
(push)
(declare-const _19-0 (_ BitVec 19))
(assert (xor v11 v2 v14 v8 (and v1 v15 v17 v10 v10 v3 v10 v4 v0)))
(push)
(declare-const v19 Bool)
(assert (not v12))
(push)
(declare-const v20 Bool)
(assert (xor (not v12) v18 (xor v11 v2 v14 v8 (and v1 v15 v17 v10 v10 v3 v10 v4 v0)) v15 v15 (not v4) v3 v11 v5 v10 v17))
(assert (xor v2 (xor (not v12) v18 (xor v11 v2 v14 v8 (and v1 v15 v17 v10 v10 v3 v10 v4 v0)) v15 v15 (not v4) v3 v11 v5 v10 v17) v13 (bvsge (bvadd _19-0 _19-0) (bvurem _19-0 _19-0)) (not v12) v8 v12))
(check-sat)
(declare-const _16-0 (_ BitVec 16))
(assert (xor v3 (not v12) v15 (xor v11 v2 v14 v8 (and v1 v15 v17 v10 v10 v3 v10 v4 v0)) v20 (and (not v4) v13 v17 v19 v10 (xor v11 v2 v14 v8 (and v1 v15 v17 v10 v10 v3 v10 v4 v0)) v0 v8 v4 v1) v19 v20))
(push)
(declare-const v21 Bool)
(declare-const _30-0 (_ BitVec 30))
(assert (exists ((q0 (_ BitVec 19)) (q1 (_ BitVec 19)) (q2 (_ BitVec 30)) (q3 (_ BitVec 10))) (=> (bvugt (_ bv515 10) q3) (distinct _30-0 _30-0 _30-0 q2 _30-0))))
(check-sat)
